T:Type, P:(T), L_1, L_2:T List.
L_2  filter(P;L_1)  (L_3:T List. L_3  L_1 & L_2 = filter(P;L_3)) 

latex

Definitions	, x:A. B(x), t  T, P  Q, x:A. B(x), P & Q, l1  l2, Prop, filter(P;l), P  Q, P  Q, i  j < k, AB, {i..j}, b, Unit, b, A, {T}, False
Lemmas	cons iseg, implies functionality wrt iff, nil iseg, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, assert of null, iseg nil, iseg weakening, firstn is iseg, filter wf, iseg wf, bool wf